T:Type, L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x])) 

latex

Definitions	t  T, x:A. B(x), ||as||, Prop, P  Q, x:A. B(x), P & Q, P  Q, b, i=j, P  Q, Dec(P), ij, as @ bs, a  b, False, A
Lemmas	append wf, non neg length, decidable assert, eq int wf, assert of eq int, neg assert of eq int, length wf1